Nuprl Lemma : gen_hyp_tp
12,41
postcript
pdf
A
:Type{i},
e
:
A
,
H
:(
A
Type{j}),
z
:
H
(
e
).
z
0
latex
ProofTree
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
x
:
A
.
B
(
x
)
origin
A:Type{i}, e:A, H:(A
Type{j}), z:H(e). z 
0 
A:Type{i}, e:A, H:(AType{j}), z:H(e). z 0
Tx:A. B(x)
x:A. B(x)